#!/usr/bin/python
#oracle_abstain
import re
import os
import sys

debug = False

lines = sys.stdin.readlines()

lemma = sys.argv[1]
if debug: print >> sys.stderr, "Lemma is "+lemma

priorities = []

def prioritize(num,m):
  global priorities, plist, match
  for i in range(len(priorities)):
    if match:
      if re.match(priorities[i],m):
         plist[i].append(num)
         break
    else:
      if priorities[i] in m:
         plist[i].append(num)
         break

if lemma == "functional":
  match = False
  priorities = ["'proofV'","'proofY'","PeqP",
"'BB', <'codes","!KU( ~skS","BB_C","codeBBOther","In_S( 'H","In_S( $D","AgSt","BB_","In_A( 'BB","!KU( ~r","cp(", "In_S","In_A","~~>","cp("]


if lemma == "indivVerif":
  match = False
  priorities = ["AgSt_H","In_A( 'S', <'codes'","In_A( 'BB', <'codes'","In_S","In_A","In_S( 'H1'","~~>","cp("]
if lemma == "Universal_VerProofV_v1":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofV'","PeqPVote","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofV_v2":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofV'","PeqPVote","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofV_v3":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofV'","PeqPVote","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofV_v4":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofV'","PeqPVote","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofV_v5":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofV'","PeqPVote","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofV_v6":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofV'","PeqPVote","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofV_v7":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofV'","PeqPVote","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofV_v8":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofV'","PeqPVote","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofY_v1":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofY'","PeqPY","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofY_v2":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofY'","PeqPY","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofY_v3":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofY'","PeqPY","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofY_v4":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofY'","PeqPY","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofY_v5":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofY'","PeqPY","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofY_v6":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofY'","PeqPY","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofY_v7":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofY'","PeqPY","In_S","In_A","In_S( 'H1'","~~>","cp("]

if lemma == "Universal_VerProofY_v8":
  match = False
  priorities = ["!KU( ~skS","In_S( 'H1', 'D1', vote","In_S( 'H2', 'D2', vote", "PeqPVote","AgSt_Au(", "'codes'","proofY'","PeqPY","In_S","In_A","In_S( 'H1'","~~>","cp("]
 
#if lemma == "Device_authentication":
#  match = False
#  priorities = [ "AgentState", "senc", "~skS.3", "~skS.1", "~rD.1", "~rS.1", "~pw", "~rS", "~rD" ]

#j
plist = [ [] for i in priorities ]

for line in lines:
  if debug: print >> sys.stderr, "Line is "+line,

  num = line.split(':')[0]

#  if lemma == "secret":
  prioritize(num,line)
#    if debug: print >> sys.stderr, "Current list: ",plist
#  else:
#    sys.exit(0)

for j in range(len(plist)):
  for i in plist[j]:
    print i
print 1
